feat: BitVec.eq_of_getElem_eq#5213
Conversation
github-actions
bot
added
the
toolchain-available
|
Mathlib CI status (docs):
|
src/Init/Data/BitVec/Lemmas.lean
Outdated
| omega | ||
|
|
||
| theorem eq_of_getElem_eq {x y : BitVec w} | ||
| (pred : ∀ (i : Fin w), x[i] = y[i]) : x = y := by |
There was a problem hiding this comment.
I think the preferred spelling of this would be to use Nat instead of Fin to be consistent with the bits of the API added in #5200.
| (pred : ∀ (i : Fin w), x[i] = y[i]) : x = y := by | |
| (pred : ∀ (i : Nat) (_ : i < w), x[i] = y[i]) : x = y := by |
See also the analogous lemma List.ext_getElem.
There was a problem hiding this comment.
It seems for BitVec we used historically:
theorem eq_of_getLsbD_eq {x y : BitVec w}
(pred : ∀(i : Fin w), x.getLsbD i.val = y.getLsbD i.val) : x = y := by
theorem eq_of_getMsbD_eq {x y : BitVec w}
(pred : ∀(i : Fin w), x.getMsbD i.val = y.getMsbD i.val) : x = y := byI guess we should at the very least remain consistent within BitVec.
I now added both variants to this PR and ported one theorem to show the code impact. Happy to flip to Nat, but would appreciate a comment why this is preferable over Fin.
|
I don't think it's a good idea to prove theorems about |
| theorem getElem_eq_toNat_testBit (x : BitVec w) (i : Fin w) : | ||
| x[i] = x.toNat.testBit i := rfl |
There was a problem hiding this comment.
This should use separate i : Nat and h : i < w arguments, otherwise it's only applicable for getElem of the coercion of a Fin.
|
@tobiasgrosser, e.g. my first steps here would be #5247. |
|
This was resolved in #5247. |
3 participants
No description provided.